es:event_system{i:l}, e1,e2:es-E(es), P:({e:es-E(es)| loc(e) = loc(e1)  Id} prop{i:l}).
(loc(e2) = loc(e1)  Id)  (e[e1,e2].P(e)  prop{i:l}) 

latex

Definitions	t  T, b, P  Q, False, A, x:A. B(x), loc(e), Id, event_system{i:l}, es-E(es), prop{i:l}, x(s), es-le(es; e; e'), e[e1,e2].P(e)
Lemmas	es-le wf, es-E wf, event system wf, Id wf, es-loc wf, es-le-loc, es-loc-pred